Nuprl Lemma : es-empty-interface-property
11,40
postcript
pdf
es
:ES. es-interface-empty(
es
;Empty)
latex
Definitions
es-interface-empty(
es
;
I
)
,
b
,
isempty{isempty_compseq_tag_def:ObjectId}(
e
)
,
A
,
E
,
ES
,
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
t
T
,
s
=
t
Lemmas
event
system
wf
,
es-E
wf
origin
es:ES. es-interface-empty(es;Empty) es:ES. es-interface-empty(es;Empty) 
b
Ax:A. B(x)
B(x)
T